r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a). Carrier(r/d)  Type 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, Ideal(r){i}, Carrier(r/d)
Definitions	Carrier(r/d), t  T, x:A. B(x), x,y. t(x;y), x f y, , P & Q, P  Q, P  Q, False, Rng, Ideal(r){i}, CRng, x(s1,s2), P  Q, T, detach_fun(T;A), {T}, XM, A, P  Q, Dec(P)
Lemmas	crng wf, ideal wf, rng car wf, detach fun wf, quotient wf, rng minus wf, rng plus wf, assert wf, detach fun properties, squash wf, equiv rel functionality wrt iff, stable from decidable, sq stable from stable, squash elim, ideal defines eqv, ideal p wf